Definitions | t T, Void, x:A.B(x), x:A B(x), P  Q, x:A. B(x), x dom(f), , f g, x : v, fpf-normalize(eq;g), x:A B(x), a:A fp B(a), Type, EqDecider(T), f(a), x(s),  x. t(x), Top, s = t, [], ff, eqof(d), p  q,  b, x.A(x), filter(P;l), [car / cdr], reduce(f;k;as), , <a, b>, f(x), f(x)?z, t.1, s ~ t, deq-member(eq;x;L), , {T}, SQType(T), b, A, , P & Q, P   Q, Unit, left + right, type List, False, tt, p  q, (x l), True, P  Q |